D:dsys{i:l}, P:({es:ES{i}| d-es{i:l}(D; es) }Prop{i'}).
d-realizes2{i:l}(D; es.P(es))  d-realizes{i:l}(D; es.P(es)) 

latex

Definitions	x. t(x), ES, es is an event system of D, Prop, D realizes2 es.P(es), D realizes es. P(es), x(s), PossibleWorld(D;w), FairFifo, World, D1  D2, Dsys, x:A. B(x), P  Q, t  T
Lemmas	dsys wf, d-sub wf, world wf, fair-fifo wf, possible-world wf, d-es wf, event system wf, d-realizes2 wf, possible-world-monotonic